Curry-Howard correspondence